$\exists$${\it code}$:$\mathbb{N}\rightarrow$($k$:$\mathbb{N}$ $\times$ (\{0..$k$$^{-}$\}$\rightarrow\mathbb{N}$)). Surj($\mathbb{N}$;$k$:$\mathbb{N}$ $\times$ (\{0..$k$$^{-}$\}$\rightarrow\mathbb{N}$);${\it code}$)